COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	
C00014 ENDMK
C⊗;
;;;
(wipe-out)
(get-proofs lispax)
(proof flat)
(context lispax#1:*)

;;; flat(x,u) has an imbedded call which makes proofs more difficult.
(decl (flat) |ground⊗ground→ground| constant)

(axiom |∀x u.flat(x,u) = if atom x then x~u else flat(car x,flat(cdr x, u))|)
(lname definfo)

(decl (flatten) |ground → ground| constant)

(axiom |∀x.flatten(x) = if atom x then list(x)
                        else flatten(car x)*flatten(cdr x)|)
(lname definfo)

(∀E PHI |λX.∀U.LISTP FLAT(X,U)| sexpinduction
|nil*([1#1#1]($definfo**sortinfo))*nil*([1#2#1#2]($definfo**sortinfo))
**simpinfo*nil*([1](der))*nil|
 sortinfo)

(∀e phi |λx.listp flatten(x)| sexpinduction
|nil*([1#1#1]($definfo*nil**simpinfo*nil))*nil
*([1#1#2](&definfo*nil**simpinfo*nil))*([1#1](imp(listappend)*der))*nil|
 sortinfo)
(lname listpflatten)

(∀e phi |λx.∀u.flat(x,u)=flatten(x)*u| sexpinduction
|nil*([1#1#1](&definfo*nil*$definfo**simpinfo*nil))*nil
*([1#1#2](&definfo**simpinfo*nil))|
listpflatten sortinfo)

(assume |(∀u.flat(x,u)=flatten(x)*u)∧(∀u.flat(y,u)=flatten(y)*u)|)

(trw |flat(x,flat(y,u))| |*-1| listpflatten sortinfo)

(∀i u)

(ci -3 -1)

(∀i (x y))

(trw |∀x u.flat(x,u) = flatten(x)*u| |imp(-6,-1)*taut|)

(∀e phi |λx.∀u.flat(x,u)=flatten(x)*u| sexpinduction
|nil|
listpflatten sortinfo)

(∀e phi |λx.∀u.flat(x,u)=flatten(x)*u| sexpinduction
|nil*([1#1#1](&definfo*$simpinfo*nil))|
listpflatten sortinfo)

(∀e phi |λx.∀u.flat(x,u)=flatten(x)*u| sexpinduction
|nil*([1#1#1](&definfo*$simpinfo*nil*$definfo*nil))|
listpflatten sortinfo)

(∀e phi |λx.∀u.flat(x,u)=flatten(x)*u| sexpinduction
|nil*([1#1#1](&definfo*$simpinfo*nil*$definfo**simpinfo*nil))|
listpflatten sortinfo)

(∀e phi |λx.∀u.flat(x,u)=flatten(x)*u| sexpinduction
|nil*([1#1#1](&definfo*$simpinfo*nil*$definfo**simpinfo*nil))*nil|
listpflatten sortinfo)

(∀e phi |λx.∀u.flat(x,u)=flatten(x)*u| sexpinduction
|nil*([1#1#1](&definfo*nil*$definfo**simpinfo*nil))*nil|
listpflatten sortinfo)

(∀e phi |λx.∀u.flat(x,u)=flatten(x)*u| sexpinduction
|nil*([1#1#1](&definfo*nil*$definfo**simpinfo*nil))*nil
*([1#1#2](&definfo**simpinfo))|
listpflatten sortinfo)

(∀E PHI |λX.∀U.LISTP FLAT(X,U)| sexpinduction
|nil*([1#1#1]($definfo**sortinfo))|
 sortinfo)

(∀E PHI |λX.∀U.LISTP FLAT(X,U)| sexpinduction
|nil*([1#1#1]($definfo**sortinfo*nil))|
 sortinfo)

(∀E PHI |λX.∀U.LISTP FLAT(X,U)| sexpinduction
|nil*([1#1#1]($definfo*nil**sortinfo*nil))|
 sortinfo)

(∀E PHI |λX.∀U.LISTP FLAT(X,U)| sexpinduction
|nil*([1#1#1]($definfo*nil**sortinfo*nil))*nil|
 sortinfo)

(∀E PHI |λX.∀U.LISTP FLAT(X,U)| sexpinduction
|nil*([1#1#1]($definfo*nil**sortinfo*nil))*nil
*([1#1#2]($definfo*nil*sortinfo*nil))|
 sortinfo)

(∀E PHI |λX.∀U.LISTP FLAT(X,U)| sexpinduction
|nil*([1#1#1]($definfo*nil**sortinfo*nil))*nil
*([1#1#2]($definfo*nil*sortinfo*nil))*nil|
 sortinfo)

(∀E PHI |λX.∀U.LISTP FLAT(X,U)| sexpinduction
|nil*([1#1#1]($definfo*nil**sortinfo*nil))*nil
*([1#1#2]($definfo*nil*sortinfo*nil))*sortinfo*nil|
 sortinfo)

;;;;
(∀E PHI |λX.∀U.LISTP FLAT(X,U)| sexpinduction
|nil*([1#1#1]($definfo**sortinfo))*nil*([1#2#1#2]($definfo**sortinfo))
**simpinfo*nil*([1](der))*nil|
 sortinfo)